<html>
<head><meta charset="utf-8"><title>design meeting 2019.11.11 · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html">design meeting 2019.11.11</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="180448354"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180448354" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180448354">(Nov 11 2019 at 18:42)</a>:</h4>
<p>Hey <span class="user-group-mention" data-user-group-id="692">@WG-traits</span> -- so for today's design meeting I was thinking we could talk over the work that <span class="user-mention" data-user-id="232957">@Jack Huey</span> has been doing around handling co-induction in the chalk engine (it's currently unsound; rustc used to be unsound in the same way but we fixed it, albeit in a rather inefficient fashion). We've got a <a href="https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA" target="_blank" title="https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA">kind of writeup</a> here summarizing some of the problems and a proposed solution.</p>



<a name="180448359"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180448359" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180448359">(Nov 11 2019 at 18:42)</a>:</h4>
<p>Anyway that starts in ~20 minutes</p>



<a name="180449875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180449875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180449875">(Nov 11 2019 at 19:01)</a>:</h4>
<p><span aria-label="wave" class="emoji emoji-1f44b" role="img" title="wave">:wave:</span> <span class="user-group-mention" data-user-group-id="692">@WG-traits</span> -- design meeting start?</p>



<a name="180449989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180449989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180449989">(Nov 11 2019 at 19:02)</a>:</h4>
<p>So yeah  as I wrote above I thought we'd focus for today on this coinduction problem</p>



<a name="180449997"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180449997" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180449997">(Nov 11 2019 at 19:02)</a>:</h4>
<p>But maybe it's worth giving a bit of context :)</p>



<a name="180450002"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450002" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450002">(Nov 11 2019 at 19:02)</a>:</h4>
<p>Not sure who's around today</p>



<a name="180450052"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450052" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450052">(Nov 11 2019 at 19:03)</a>:</h4>
<p>So let me ask this -- while I run to get a glass of water -- please <span aria-label="wave" class="emoji emoji-1f44b" role="img" title="wave">:wave:</span> if you feel you want me to cover what the heck coinduction has to do with trait solving and/or auto traits</p>



<a name="180450167"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450167" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450167">(Nov 11 2019 at 19:04)</a>:</h4>
<p>I think I mostly understand it at this point?</p>



<a name="180450179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450179">(Nov 11 2019 at 19:04)</a>:</h4>
<p>(not sure if anyone else is around)</p>



<a name="180450186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450186">(Nov 11 2019 at 19:04)</a>:</h4>
<p>I see a few waves above :)</p>



<a name="180450250"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450250" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450250">(Nov 11 2019 at 19:06)</a>:</h4>
<p>OK, well, the TL;DR is that coinductive solving is "trait solving where cycles are ok", and we use it for auto traits :)</p>



<a name="180450303"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450303" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450303">(Nov 11 2019 at 19:06)</a>:</h4>
<p>but at some point I realized that the existing chalk solver has a bug here</p>



<a name="180450322"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450322" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450322">(Nov 11 2019 at 19:06)</a>:</h4>
<p>actually the bug cropped up first in rustc, which had the same bug</p>



<a name="180450333"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450333" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450333">(Nov 11 2019 at 19:06)</a>:</h4>
<p>this is <a href="https://github.com/rust-lang-nursery/chalk/issues/248" target="_blank" title="https://github.com/rust-lang-nursery/chalk/issues/248">chalk#248</a></p>



<a name="180450346"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450346" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450346">(Nov 11 2019 at 19:06)</a>:</h4>
<p>the example being</p>
<div class="codehilite"><pre><span></span>C1 :- C2, C3.
C2 :- C1.
</pre></div>



<a name="180450374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450374">(Nov 11 2019 at 19:07)</a>:</h4>
<p>you can think of <code>C1</code> as "co-inductive" goal, like maybe <code>Foo: Send</code></p>



<a name="180450400"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450400" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450400">(Nov 11 2019 at 19:07)</a>:</h4>
<p>or maybe better, just think of it as short for <code>Implemented(C1: Send)</code></p>



<a name="180450472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450472">(Nov 11 2019 at 19:08)</a>:</h4>
<p>anyway, the problem here is that <code>C1</code> and <code>C2</code> should not be provable, as there is no rule to prove <code>C3</code></p>



<a name="180450492"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450492" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450492">(Nov 11 2019 at 19:08)</a>:</h4>
<p>unfortunately, if you execute things in the wrong order, our existing solver would conclude that <code>C2</code> is true</p>



<a name="180450537"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450537" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450537">(Nov 11 2019 at 19:09)</a>:</h4>
<p>the reason is because of caching, in short</p>



<a name="180450552"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450552" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450552">(Nov 11 2019 at 19:09)</a>:</h4>
<p>basically we would start to prove <code>C1</code>...</p>



<a name="180450558"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450558" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450558">(Nov 11 2019 at 19:09)</a>:</h4>
<p>...and then try to prove <code>C2</code>...</p>



<a name="180450577"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450577" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450577">(Nov 11 2019 at 19:09)</a>:</h4>
<p>proving <code>C2</code> recursively requires proving <code>C1</code>, but this is coinductive, so "cycles are ok", and hence we conclude that <code>C2</code> holds (and we cache this)</p>



<a name="180450647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450647">(Nov 11 2019 at 19:10)</a>:</h4>
<p>...then we continue trying to prove <code>C1</code> and we encounter <code>C3</code> -- but <code>C3</code> cannot be proven (no rules for that), so we conclude that <code>C1</code> is not true</p>



<a name="180450665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450665">(Nov 11 2019 at 19:10)</a>:</h4>
<p>but we still have a cached result saying that <code>C2</code> is true</p>



<a name="180450688"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450688" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450688">(Nov 11 2019 at 19:10)</a>:</h4>
<p>our sol'n in rustc was basically just not to cache anything if a cycle occurs, but sometimes this can lead to us doing a lot of extra work</p>



<a name="180450705"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450705" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450705">(Nov 11 2019 at 19:10)</a>:</h4>
<p>the underlying problem here is that it is a simplification to say that "cycles are ok"</p>



<a name="180450769"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450769" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450769">(Nov 11 2019 at 19:11)</a>:</h4>
<p>coinduction is really about everything being "internally consistent", so to speak. "True until proven false" might be a good intuition :)</p>



<a name="180450834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450834">(Nov 11 2019 at 19:12)</a>:</h4>
<p>So here C2 was true, assuming C1 was true; but C1 wasn't.</p>



<a name="180450840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450840">(Nov 11 2019 at 19:12)</a>:</h4>
<p>(Make sense?)</p>



<a name="180450940"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180450940" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180450940">(Nov 11 2019 at 19:13)</a>:</h4>
<p>OK, so I guess I'll outline briefly the fix that I had in mind, but I'm curious to hear <span class="user-mention" data-user-id="232957">@Jack Huey</span>'s latest thoughts as well</p>



<a name="180451064"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451064" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451064">(Nov 11 2019 at 19:15)</a>:</h4>
<p>trying to decide where to begin in the explanation :)</p>



<a name="180451073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451073">(Nov 11 2019 at 19:15)</a>:</h4>
<p>I'll real fast loop back</p>



<a name="180451093"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451093" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451093">(Nov 11 2019 at 19:15)</a>:</h4>
<p>the solver has this notion of "tables" -- basically, when you're trying to prove some goal like <code>C1</code>, it creates a table for that goal, and within each goal it has a number of strands --</p>



<a name="180451096"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451096" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451096">(Nov 11 2019 at 19:15)</a>:</h4>
<p>each strand is like "some viable way prove that goal"</p>



<a name="180451154"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451154" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451154">(Nov 11 2019 at 19:16)</a>:</h4>
<p>the strand has two bits of state, a substitution (values for any inference variables in the goal) and a set of subgoals (things left to prove)</p>



<a name="180451165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451165">(Nov 11 2019 at 19:16)</a>:</h4>
<p>so when we start to prove <code>C1</code>, we would make a table for that goal, and then look for any rules we can use to prove it</p>



<a name="180451170"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451170" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451170">(Nov 11 2019 at 19:16)</a>:</h4>
<p>in this case, there is just one, <code>C1 :- C2, C3</code></p>



<a name="180451193"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451193" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451193">(Nov 11 2019 at 19:16)</a>:</h4>
<p>so we would create a strand with an empty substitution (no inference variables in this simple example) and two subgoals (<code>[C2, C3])</code></p>



<a name="180451212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451212">(Nov 11 2019 at 19:16)</a>:</h4>
<p>this is called an <code>ExClause</code> in the code</p>



<a name="180451224"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451224" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451224">(Nov 11 2019 at 19:17)</a>:</h4>
<p>that comes from some papers I was reading, which called it an <code>X-clause</code></p>



<a name="180451271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451271">(Nov 11 2019 at 19:17)</a>:</h4>
<p>anyway, the idea here is to extend that list of subgoals with a list of <em>delayed subgoals</em> -- basically, things we had to assume were true due to a coinductive cycle, but they are not fully proven yet</p>



<a name="180451344"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451344" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451344">(Nov 11 2019 at 19:18)</a>:</h4>
<p>(maybe delayed isn't the best name, I'm somewhat adopting terminology the papers were using for handling other things, but the concept seems very similar to me)</p>



<a name="180451369"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451369" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451369">(Nov 11 2019 at 19:18)</a>:</h4>
<p>so in particular when we go to solve <code>C2</code>, and we encounter the subgoal of proving <code>C1</code>, we would find there is a cycle;</p>



<a name="180451370"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451370" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451370">(Nov 11 2019 at 19:18)</a>:</h4>
<p>I think delayed works. Or <code>coinductive</code></p>



<a name="180451374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451374">(Nov 11 2019 at 19:18)</a>:</h4>
<p>but instead of just considering it <em>true</em></p>



<a name="180451381"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451381" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451381">(Nov 11 2019 at 19:18)</a>:</h4>
<p>we would make it <em>delayed</em></p>



<a name="180451419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451419">(Nov 11 2019 at 19:19)</a>:</h4>
<p>the notation I used in the hackmd for an <code>ExClause</code> is <code>Goal :- DelayedSubgoals | Subgoals</code></p>



<a name="180451427"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451427" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451427">(Nov 11 2019 at 19:19)</a>:</h4>
<p>which...is kind of arcane</p>



<a name="180451433"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451433" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451433">(Nov 11 2019 at 19:19)</a>:</h4>
<p>but I guess I'll run with it</p>



<a name="180451460"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451460" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451460">(Nov 11 2019 at 19:19)</a>:</h4>
<p>so if we had <code>C2 :- | C1</code> (no delayed goals, just one subgoal)</p>



<a name="180451473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451473">(Nov 11 2019 at 19:19)</a>:</h4>
<p>we would convert it to <code>C2 :- C1 |</code> (now <code>C1</code> is delayed)</p>



<a name="180451540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451540">(Nov 11 2019 at 19:20)</a>:</h4>
<p>maybe better to use a notation like <code>{ substitition: [], delayed: [C1], subgoals: [] }</code> :)</p>



<a name="180451560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451560">(Nov 11 2019 at 19:20)</a>:</h4>
<p>well anyway the point is that this delay list can propagate into the answer</p>



<a name="180451590"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451590" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451590">(Nov 11 2019 at 19:20)</a>:</h4>
<p>so where the thing we cache as the "answer" for <code>C2</code> used to just be "true", it's now (effectively) "true if C1 is true"</p>



<a name="180451597"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451597" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451597">(Nov 11 2019 at 19:20)</a>:</h4>
<p>note that this remains valid even if C1 turns out to be false</p>



<a name="180451680"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451680" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451680">(Nov 11 2019 at 19:21)</a>:</h4>
<p>so where an "answer" used to be <code>{ substitution, region_constraints }</code> (we can ignore region constraints here), it is now <code>{ substitution, delayed, region_constriants }</code></p>



<a name="180451691"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451691" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451691">(Nov 11 2019 at 19:22)</a>:</h4>
<p>and when we incorporate an answer, we have to add those delayed goals to our own subgoal list</p>



<a name="180451760"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451760" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451760">(Nov 11 2019 at 19:22)</a>:</h4>
<p>so the strand for C1 starts as</p>



<a name="180451770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451770">(Nov 11 2019 at 19:22)</a>:</h4>
<p>Well, also an answer can be ambiguous too</p>



<a name="180451780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451780">(Nov 11 2019 at 19:22)</a>:</h4>
<ul>
<li><code>{ subgoals: [C2, C3] }</code></li>
</ul>



<a name="180451789"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451789" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451789">(Nov 11 2019 at 19:22)</a>:</h4>
<p>(yeah, I'm ignoring things that aren't too relevant)</p>



<a name="180451806"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451806" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451806">(Nov 11 2019 at 19:23)</a>:</h4>
<ul>
<li>it then gets an answer <code>{ delayed: [C1] }</code> from the <code>C2</code> table</li>
</ul>



<a name="180451841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451841">(Nov 11 2019 at 19:23)</a>:</h4>
<ul>
<li>so it converts its state to <code>{ subgoals: [C3, C1] }</code> -- i.e., it removed <code>C2</code> (which was proven) but added the delayed subgoal</li>
</ul>



<a name="180451852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451852">(Nov 11 2019 at 19:23)</a>:</h4>
<ul>
<li>at that point, it will fail to prove C3</li>
</ul>



<a name="180451856"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451856" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451856">(Nov 11 2019 at 19:23)</a>:</h4>
<p>and so it just gets an error</p>



<a name="180451880"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451880" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451880">(Nov 11 2019 at 19:23)</a>:</h4>
<p>but then later if we try to use the answer from C2 in some other context, it too will fail to prove C1</p>



<a name="180451884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451884">(Nov 11 2019 at 19:23)</a>:</h4>
<p>so everything works out ok</p>



<a name="180451895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451895">(Nov 11 2019 at 19:23)</a>:</h4>
<p>(at least that's the idea :)</p>



<a name="180451945"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180451945" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180451945">(Nov 11 2019 at 19:24)</a>:</h4>
<p>(make sense so far?)</p>



<a name="180452215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452215">(Nov 11 2019 at 19:26)</a>:</h4>
<p>one thing worth mentioning: if <code>C3</code> <em>were</em> provable, then the <code>C1</code> strand would have gone to a state like <code>{ subgoals: [C1] }</code>.</p>



<a name="180452250"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452250" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452250">(Nov 11 2019 at 19:27)</a>:</h4>
<p>the key point is that here we a <em>trivial</em> coinductive cycle -- basically <code>C1</code> is true if `C1 is true -- and <em>that</em> we can just ignore as clearly true</p>



<a name="180452286"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452286" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452286">(Nov 11 2019 at 19:27)</a>:</h4>
<p>we don't have the caching concerns because C1 is exactly the thing we are now proving, so if we fail, no answer is produced, and if we succeed, then the answer is valid</p>



<a name="180452328"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452328" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452328">(Nov 11 2019 at 19:27)</a>:</h4>
<p>anyway, ok, that's the high-level idea, but there are a few tricky bits --</p>



<a name="180452416"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452416" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452416">(Nov 11 2019 at 19:28)</a>:</h4>
<p>I'll stop here for the moment, though. I want to leave room for questions, but also check in with <span class="user-mention" data-user-id="232957">@Jack Huey</span></p>



<a name="180452451"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452451" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452451">(Nov 11 2019 at 19:28)</a>:</h4>
<p>I saw you mentioned that you had some of the impl work on this strategy</p>



<a name="180452454"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452454" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452454">(Nov 11 2019 at 19:28)</a>:</h4>
<p>I think everything makes sense so conceptually</p>



<a name="180452469"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452469" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452469">(Nov 11 2019 at 19:28)</a>:</h4>
<p>Yeah, I have the key idea implemented</p>



<a name="180452511"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452511" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452511">(Nov 11 2019 at 19:29)</a>:</h4>
<p>I'm not doing something correctly in terms of canonicalization I think</p>



<a name="180452607"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452607" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452607">(Nov 11 2019 at 19:30)</a>:</h4>
<p>Basically though, implementation wise it's pretty similar to how you imagined it</p>



<a name="180452642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452642">(Nov 11 2019 at 19:30)</a>:</h4>
<p>OK</p>



<a name="180452652"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452652" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452652">(Nov 11 2019 at 19:30)</a>:</h4>
<p>the delayed subgoals I have on <code>Answer</code> though, instead of <code>CanonicalConstrainedSubst</code></p>



<a name="180452665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452665">(Nov 11 2019 at 19:30)</a>:</h4>
<p>Ok, yes. I think that's wrong :)</p>



<a name="180452673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452673">(Nov 11 2019 at 19:31)</a>:</h4>
<blockquote>
<p>I'm not doing something correctly in terms of canonicalization I think</p>
</blockquote>
<p>and probably related to this</p>



<a name="180452691"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452691" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452691">(Nov 11 2019 at 19:31)</a>:</h4>
<p>in particular, I think the delayed subgoals and the substitution must be canonicalized together</p>



<a name="180452701"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452701" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452701">(Nov 11 2019 at 19:31)</a>:</h4>
<p>hmm</p>



<a name="180452711"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452711" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452711">(Nov 11 2019 at 19:31)</a>:</h4>
<p>(because they share inference variables)</p>



<a name="180452740"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452740" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452740">(Nov 11 2019 at 19:31)</a>:</h4>
<p>that makes sense I think</p>



<a name="180452793"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452793" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452793">(Nov 11 2019 at 19:32)</a>:</h4>
<p>just means that now we will need to pass a <code>Context</code> type through a lot more</p>



<a name="180452855"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452855" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452855">(Nov 11 2019 at 19:32)</a>:</h4>
<p>Since a <code>Literal</code> is over <code>C::GoalInEnvironment</code></p>



<a name="180452878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452878">(Nov 11 2019 at 19:32)</a>:</h4>
<p>if you imagine a rule like</p>
<div class="codehilite"><pre><span></span>C1(X, Y) :- C2(X, Y)
C2(X, Y) :- C1(Y, X)
</pre></div>


<p>then the result for <code>C2</code> will be something like</p>
<div class="codehilite"><pre><span></span>{ substitution: [^0, ^1], delayed: C1(^1, ^0) }
</pre></div>



<a name="180452900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452900">(Nov 11 2019 at 19:33)</a>:</h4>
<p>which also got me thinking: in what cases (if ever) would we have a delayed subgoal on a negative literal?</p>



<a name="180452921"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452921" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452921">(Nov 11 2019 at 19:33)</a>:</h4>
<p>never, I think</p>



<a name="180452989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180452989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180452989">(Nov 11 2019 at 19:34)</a>:</h4>
<p>since we only delay on fully coinductive cycles, and I don't think those should include negation</p>



<a name="180453015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453015">(Nov 11 2019 at 19:34)</a>:</h4>
<p>It doesn't pop up in any current tests</p>



<a name="180453020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453020">(Nov 11 2019 at 19:34)</a>:</h4>
<p>which is why I asked</p>



<a name="180453090"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453090" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453090">(Nov 11 2019 at 19:35)</a>:</h4>
<p>so certainly when proving <code>not { G }</code>, we should never encounter a cycle on <code>G</code>, I think we already kind of assert this, right?</p>



<a name="180453151"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453151" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453151">(Nov 11 2019 at 19:36)</a>:</h4>
<p>Right, that would be a <code>NegativeCycle</code></p>



<a name="180453165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453165">(Nov 11 2019 at 19:36)</a>:</h4>
<p>but it is plausible to have something like <code>not { C2 }</code> (to build on our example), where the answer would have delayed subgoals</p>



<a name="180453200"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453200" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453200">(Nov 11 2019 at 19:37)</a>:</h4>
<p>but I think those should be "refinable" (i.e., as in our example, we could then go and prove <code>C1</code>)</p>



<a name="180453207"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453207" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453207">(Nov 11 2019 at 19:37)</a>:</h4>
<p>the only reason that would fail is if there is a cycle that includes the negative edge</p>



<a name="180453218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453218">(Nov 11 2019 at 19:37)</a>:</h4>
<p>and I think we want to assert that this doesn't happen by construction</p>



<a name="180453297"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453297" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453297">(Nov 11 2019 at 19:38)</a>:</h4>
<blockquote>
<p>but I think those should be "refinable" (i.e., as in our example, we could then go and prove <code>C1</code>)</p>
</blockquote>
<p>this comes back to that note I had about how <code>ensure_root_answer</code> can do refining, but it's really not "special" in this regard</p>



<a name="180453319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453319">(Nov 11 2019 at 19:38)</a>:</h4>
<p>but of course we're way in the weeds here, I doubt anyone else has any idea what I'm talking about</p>



<a name="180453327"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453327" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453327">(Nov 11 2019 at 19:38)</a>:</h4>
<p>(though I'm not clear if anyone else is here today...)</p>



<a name="180453374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453374">(Nov 11 2019 at 19:39)</a>:</h4>
<p>(does that make any sense, <span class="user-mention" data-user-id="232957">@Jack Huey</span>?)</p>



<a name="180453380"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453380" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453380">(Nov 11 2019 at 19:39)</a>:</h4>
<p>I think so</p>



<a name="180453389"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453389" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453389">(Nov 11 2019 at 19:39)</a>:</h4>
<p>I have to think about it a bit more</p>



<a name="180453472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453472">(Nov 11 2019 at 19:40)</a>:</h4>
<p>Probably worth a test, either for panic or pass</p>



<a name="180453473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453473">(Nov 11 2019 at 19:40)</a>:</h4>
<p>I guess an example which we do NOT want would be</p>
<div class="codehilite"><pre><span></span>C1 :- not { C2 }
C2 :- C1
</pre></div>



<a name="180453536"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453536" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453536">(Nov 11 2019 at 19:41)</a>:</h4>
<p>this would be a case where pursuing the <code>not { C2 }</code> literal would yield an answer with a delayed subgoal for something still on the stack</p>



<a name="180453601"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453601" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453601">(Nov 11 2019 at 19:42)</a>:</h4>
<p>I'm pondering how can detect that :)</p>



<a name="180453613"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453613" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453613">(Nov 11 2019 at 19:42)</a>:</h4>
<p>it might be that for now we can just assert that negative literals never have delayed subgoals</p>



<a name="180453626"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453626" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453626">(Nov 11 2019 at 19:42)</a>:</h4>
<p>I guess I have to check where we use them</p>



<a name="180453629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453629">(Nov 11 2019 at 19:42)</a>:</h4>
<p>but I think they are never for coinductive goals</p>



<a name="180453757"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453757" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453757">(Nov 11 2019 at 19:44)</a>:</h4>
<blockquote>
<p>I'm pondering how can detect that :)</p>
</blockquote>
<p>more specifically, what I would like is that <code>ensure_answer</code> can guarantee that answers it gives back only have delayed literals if those things are on the stack -- the idea being that (e.g.) the first time you invoke <code>C2</code>, from within the context of <code>C1</code>, you might get back <code>C2 :- C1 |</code>, but if you invoke it from some other context, we'd refine the answer</p>



<a name="180453815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453815">(Nov 11 2019 at 19:45)</a>:</h4>
<p>but I'm not sure the best way to detect that situation.. it feels like we should be able to use the stack minimums or something..?</p>



<a name="180453856"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453856" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453856">(Nov 11 2019 at 19:45)</a>:</h4>
<p>So I think I've seen a related problem? maybe</p>



<a name="180453868"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453868" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453868">(Nov 11 2019 at 19:46)</a>:</h4>
<p>But maybe not</p>



<a name="180453919"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453919" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453919">(Nov 11 2019 at 19:46)</a>:</h4>
<p>(this negative thing seems relevant, but also kind of a "user error" situation, so I think for now it probably suffices to panic)</p>



<a name="180453938"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453938" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453938">(Nov 11 2019 at 19:46)</a>:</h4>
<p>(that is, panic if we are pursuing a negative goal and we get back delayed literals)</p>



<a name="180453952"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453952" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453952">(Nov 11 2019 at 19:46)</a>:</h4>
<p>(well, maybe:P)</p>



<a name="180453956"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453956" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453956">(Nov 11 2019 at 19:46)</a>:</h4>
<blockquote>
<p>So I think I've seen a related problem? maybe</p>
</blockquote>
<p>what's that?</p>



<a name="180453978"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180453978" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180453978">(Nov 11 2019 at 19:47)</a>:</h4>
<p>So with your </p>
<div class="codehilite"><pre><span></span>C1 :- C2, C3.
C2 :- C1.
</pre></div>


<p>example</p>



<a name="180454076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454076">(Nov 11 2019 at 19:48)</a>:</h4>
<p>When it gets to <code>C1 :- | C3</code> (the delayed subgoal isn't incorporated since it's a trivial cycle)</p>



<a name="180454080"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454080" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454080">(Nov 11 2019 at 19:48)</a>:</h4>
<blockquote>
<p>(well, maybe:P)</p>
</blockquote>
<p>ok no I think this is true, so long as <code>not</code> is not used with co-inductive goals. The reasoning is that the answer for any inductive goal cannot have delayed things in it. This is true because anything higher on the stack will not be considered a coinductive cycle and hence would just be handled as we typically handle cycles</p>



<a name="180454107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454107">(Nov 11 2019 at 19:48)</a>:</h4>
<p>It's returning <code>C1 :- C3</code></p>



<a name="180454113"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454113" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454113">(Nov 11 2019 at 19:48)</a>:</h4>
<p>returning?</p>



<a name="180454119"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454119" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454119">(Nov 11 2019 at 19:49)</a>:</h4>
<p>So <code>ensure_root_answer</code> needs to check that</p>



<a name="180454132"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454132" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454132">(Nov 11 2019 at 19:49)</a>:</h4>
<p>from <code>ensure_answer_recursively</code></p>



<a name="180454135"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454135" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454135">(Nov 11 2019 at 19:49)</a>:</h4>
<p>no, it's not</p>



<a name="180454141"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454141" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454141">(Nov 11 2019 at 19:49)</a>:</h4>
<p>that's not an answer, as it has pending subgoals still</p>



<a name="180454167"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454167" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454167">(Nov 11 2019 at 19:49)</a>:</h4>
<p>it would rather try to prove <code>C3</code> (and fail, because there are no rules that can be used to do so)</p>



<a name="180454288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454288">(Nov 11 2019 at 19:50)</a>:</h4>
<p>err right, the "answer" that <code>ensure_root_answer</code> is on the table when <code>ensure_answer_recursively</code> returns back to <code>ensure_root_answer</code> is <code>C1 :- C3 | </code></p>



<a name="180454339"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454339" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454339">(Nov 11 2019 at 19:51)</a>:</h4>
<p>it will never get that answer in my example though</p>



<a name="180454350"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454350" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454350">(Nov 11 2019 at 19:51)</a>:</h4>
<p>that would only occur if solving <code>C3</code> resulted in a coinductive cycle</p>



<a name="180454366"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454366" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454366">(Nov 11 2019 at 19:51)</a>:</h4>
<p>Yeah, I'm not sure. I'll have to look again</p>



<a name="180454384"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454384" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454384">(Nov 11 2019 at 19:52)</a>:</h4>
<p>if the example were</p>
<div class="codehilite"><pre><span></span>C3 :- C1.
C1 :- C2, C3.
C2 :- C1.
</pre></div>


<p>and we started by proving <em>C3</em>, that could happen</p>



<a name="180454466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454466">(Nov 11 2019 at 19:52)</a>:</h4>
<p>(that's maybe a good example to walk through, actually)</p>



<a name="180454494"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454494" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454494">(Nov 11 2019 at 19:52)</a>:</h4>
<p>i.e., we would start by proving <code>C3</code></p>



<a name="180454539"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454539" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454539">(Nov 11 2019 at 19:53)</a>:</h4>
<ul>
<li>strand for <code>C3</code> is <code>{ subgoals: [C1] }</code></li>
</ul>



<a name="180454551"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454551" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454551">(Nov 11 2019 at 19:53)</a>:</h4>
<ul>
<li>we start to prove <code>C1</code> with strand <code>{ subgoals: [C2, C3] }</code></li>
</ul>



<a name="180454563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454563">(Nov 11 2019 at 19:53)</a>:</h4>
<ul>
<li>we prove <code>C2</code> with answer <code>{ delayed: [C1] }</code></li>
</ul>



<a name="180454619"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454619" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454619">(Nov 11 2019 at 19:54)</a>:</h4>
<ul>
<li>we incorporate that into our strand for <code>C1</code>, yielding <code>{ subgoals: [C3, C1] }</code> (well, maybe the <code>C1</code> is screened out earlier, but that's not too imp't)</li>
</ul>



<a name="180454644"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454644" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454644">(Nov 11 2019 at 19:54)</a>:</h4>
<ul>
<li>then we go to prove <code>C3</code> but we get a cycle, so the strand for <code>C1</code> is <code>{ delayed: [C3], subgoals: [C1] }</code></li>
</ul>



<a name="180454656"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454656" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454656">(Nov 11 2019 at 19:54)</a>:</h4>
<ul>
<li>the next subgoal is a trivial cycle, resulting in an answer for <code>C1</code> of <code>{ delayed: [C3] }</code></li>
</ul>



<a name="180454669"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454669" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454669">(Nov 11 2019 at 19:55)</a>:</h4>
<ul>
<li>that is incorporated into the strand for <code>C3</code>, yielding <code>{ subgoals: [C3] }</code></li>
</ul>



<a name="180454675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454675">(Nov 11 2019 at 19:55)</a>:</h4>
<ul>
<li>which is eventually reduced to an answer <code>{}</code> (i.e., true)</li>
</ul>



<a name="180454850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/design%20meeting%202019.11.11/near/180454850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/design.20meeting.202019.2E11.2E11.html#180454850">(Nov 11 2019 at 19:57)</a>:</h4>
<p>anyway</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>